#pragma once
#include "def.hpp"

void TraverseClauseTable(LinkClause C);
Status InitClauseStack(ClauseStack &CS);
Status InitLiteralStack(LiteralStack &LS);
Status CPush(ClauseStack &CS, LinkClause p);
Status LPush(LiteralStack &LS, LinkLiteral p);
Status CPop(ClauseStack &CS, LinkClause &p);
Status LPop(LiteralStack &LS, LinkLiteral &p);
int isSingleClause(LinkClause cc);
int FindSingleClause(LinkClause C);
int isEmptyClause(LinkClause C);
void DelClauseAndLiteral(LinkClause C, ClauseStack &Cs, LiteralStack &Ls, int num);
void RecoveryClauseAndLiteral(LinkClause C, ClauseStack &Cs, LiteralStack &Ls);
int GetV(void);
int GetV2(LinkClause C);
int GetV3(LinkClause C);
void myPrint(void);
Status DPLL(LinkClause C, int idea);
void saveRes(char filename[30], int time);

/***********************
 * param: C(子句头指针)
 * return: void
 * res: 遍历子句邻接表
***********************/
void TraverseClauseTable(LinkClause C)
{
    LinkClause p = C->next;
    while (p)
    {
        LinkLiteral q = p->L->next;
        while (q)
        {
            if (q->state)
                printf("%d ", q->num);
            q = q->next;
        }
        printf("\n");
        p = p->next;
    }
}

/***********************
 * param: CS(子句栈)
 * return: status状态码
 * res: 构造子句栈，若成功返回OK，失败返回ERROR
***********************/
Status InitClauseStack(ClauseStack &CS)
{
    CS.base = (LinkClause *)malloc(STACK_INIT_SIZE * sizeof(LinkClause));
    if (!CS.base)
        return ERROR;
    CS.top = CS.base;
    CS.stacksize = STACK_INIT_SIZE;
    return OK;
}

/***********************
 * param: CS(文字栈)
 * return: status状态码
 * res: 构造文字栈，若成功返回OK，失败返回ERROR
***********************/
Status InitLiteralStack(LiteralStack &LS)
{
    LS.base = (LinkLiteral *)malloc(STACK_INIT_SIZE * sizeof(LinkLiteral));
    if (!LS.base)
        return ERROR;
    LS.top = LS.base;
    LS.stacksize = STACK_INIT_SIZE;
    return OK;
}

/***********************
 * param: ClauseStack(子句栈),LinkClause(子句头指针)
 * return: status状态码
 * res: 入栈，若成功返回OK，失败返回ERROR
***********************/
Status CPush(ClauseStack &CS, LinkClause p)
{
    if (CS.top - CS.base >= CS.stacksize)
    {
        CS.base = (LinkClause *)realloc(CS.base, (CS.stacksize + STACKINCREMENT) * sizeof(LinkClause));
        if (!CS.base)
            return ERROR;
        CS.top = CS.base + CS.stacksize;
        CS.stacksize += STACKINCREMENT;
    }
    *CS.top++ = p;
    return OK;
}

/***********************
 * param: ClauseStack(文字栈),LinkClause(文字头指针)
 * return: status状态码
 * res: 入栈，若成功返回OK，失败返回ERROR
***********************/
Status LPush(LiteralStack &LS, LinkLiteral p)
{
    if (LS.top - LS.base >= LS.stacksize)
    {
        LS.base = (LinkLiteral *)realloc(LS.base, (LS.stacksize + STACKINCREMENT) * sizeof(LinkLiteral));
        if (!LS.base)
            return ERROR;
        LS.top = LS.base + LS.stacksize;
        LS.stacksize += STACKINCREMENT;
    }
    *LS.top++ = p;
    return OK;
}

/***********************
 * param: ClauseStack(子句栈),LinkClause(子句头指针)
 * return: status状态码
 * res: 出栈，若成功返回OK，失败返回ERROR
***********************/
Status CPop(ClauseStack &CS, LinkClause &p)
{
    if (CS.top == CS.base)
        return ERROR;
    p = *--CS.top;
    return OK;
}

/***********************
 * param: ClauseStack(文字栈),LinkClause(文字头指针)
 * return: status状态码
 * res: 出栈，若成功返回OK，失败返回ERROR
***********************/
Status LPop(LiteralStack &LS, LinkLiteral &p)
{
    if (LS.top == LS.base)
        return ERROR;
    p = *--LS.top;
    return OK;
}

/***********************
 * param: LinkClause(子句头指针)
 * return: int
 * res: 若子句不存在，返回-1，存在则返回其文字个数，文字为0个时为空子句，为1时为单子句
***********************/
int isSingleClause(LinkClause cc)
{
    if (cc->state)
    {
        int n = 0;
        LinkLiteral p = cc->L->next;
        while (p)
        {
            if (p->state)
            {
                n++;
            }
            p = p->next;
        }
        return n;
    }
    return -1;
}

/***********************
 * param: LinkClause(子句头指针)
 * return: int
 * res: 查找单子句，若找到，返回该单子句的文字序号，否则返回0
***********************/
int FindSingleClause(LinkClause C)
{
    LinkClause p = C->next;
    while (p)
    {
        if (isSingleClause(p) == 1)
        {
            LinkLiteral q = p->L->next;
            // 注意，此时并不是选第一个文字，因为我是假删除
            while (q)
            {
                if (q->state == 1)
                {
                    return q->num;
                }
                q = q->next;
            }
        }
        p = p->next;
    }
    return 0;
}

/***********************
 * param: LinkClause(子句头指针)
 * return: int
 * res: 若判断是否存在空子句，存在则返回1，若为空集返回0，否则返回2
***********************/
int isEmptyClause(LinkClause C)
{
    int x = 0;
    LinkClause p = C->next;
    while (p)
    {
        if (isSingleClause(p) == 0)
        {
            return 1;
        }
        if (isSingleClause(p) >= 1)
        {
            x = 1;
        }
        p = p->next;
    }
    if (x)
    {
        return 2;
    }
    return 0;
}

/***********************
 * param: LinkClause(文子句头指针)，ClauseStack(子句栈)，LiteralStack(文字栈)，num(文字序号)
 * return: int
 * res: 删除(标记)相应数据并将其指针存入栈中
***********************/
void DelClauseAndLiteral(LinkClause C, ClauseStack &Cs, LiteralStack &Ls, int num)
{
    Llinfo[abs(num)].state = 0;
    if (num > 0)
    {
        Llinfo[abs(num)].value = 1;
    }
    else
    {
        Llinfo[abs(num)].value = 0;
    }
    LinkClause p = C->next;
    while (p)
    {
        if (p->state)
        {
            // 如果p不为空才找
            LinkLiteral q1 = p->L->next;
            LinkLiteral q2 = p->L->next;
            // 判断是否含有该文字，若含有，则删除该子句，而不管该子句中是否含有该文字的非
            int flag = 0;
            while (q1)
            {
                if (q1->num == num)
                {
                    p->state = 0;
                    CPush(Cs, p);
                    flag = 1;
                    // 处理文字数
                    {
                        LinkLiteral t = p->L->next;
                        while (t)
                        {
                            Llinfo[abs(t->num)].count--;
                            t = t->next;
                        }
                        // 此处有大量重复操作
                        // Llinfo[abs(num)].state = 0;
                        // if (num > 0)
                        // {
                        //   Llinfo[abs(num)].value = 1;
                        // }
                        // else
                        // {
                        //   Llinfo[abs(num)].value = 0;
                        // }
                    }
                    break;
                }
                q1 = q1->next;
            }
            while (q2)
            {
                if (flag)
                    break;
                if (q2->num == -num)
                {
                    q2->state = 0;
                    LPush(Ls, q2);
                }
                q2 = q2->next;
            }
        }
        p = p->next;
    }
}

/***********************
 * param: LinkClause(子句头指针)，ClauseStack(子句栈)，LiteralStack(文字栈)
 * return: void
 * res: 恢复(标记)相应数据并将其指针出栈中
***********************/
void RecoveryClauseAndLiteral(LinkClause C, ClauseStack &Cs, LiteralStack &Ls)
{
    LinkClause p;
    LinkLiteral q;
    while (CPop(Cs, p))
    {
        p->state = 1;
        // 处理文字数
        {
            LinkLiteral t = p->L->next;
            int num, flag = 0;
            while (t)
            {
                if (t->state == 1)
                {
                    flag++;
                    num = t->num;
                }
                Llinfo[abs(t->num)].count++;
                t = t->next;
            }
            // Llinfo[abs(num)].state = 0;
            // 注意: 此处如果p为单子句，其对应的文字的真值还需恢复
            if (flag == 1)
            {
                if (num > 0)
                {
                    Llinfo[num].value = 0;
                }
                else
                {
                    Llinfo[abs(num)].value = 1;
                }
            }
        }
    }
    while (LPop(Ls, q))
    {
        q->state = 1;
        // 此处重复了很多，需要优化
        int num = q->num;
        Llinfo[abs(num)].state = 1;
        if (num > 0)
        {
            Llinfo[num].value = 1;
        }
        else
        {
            Llinfo[abs(num)].value = 0;
        }
    }
}

/***********************
 * param: void
 * return: int(v的编号)
 * res: 返回v的编号，没有就返回0
***********************/
int GetV(void)
{
    int maxNum = 0;
    // bug: i<=n忘加 = 号
    for (int i = 1; i <= n; i++)
    {
        if ((Llinfo[i].state == 1) && (Llinfo[maxNum].count < Llinfo[i].count))
        {
            maxNum = i;
        }
    }
    return maxNum;
}

/***********************
 * param: void
 * return: int(v的编号)
 * res: 返回v的编号，没有就返回0
***********************/
int GetV2(LinkClause C)
{
    int maxNum = 0;
    LinkClause p = C->next;
    while (p)
    {
        if (p->state == 1)
        {
            LinkLiteral q = p->L->next;
            while (q)
            {
                if (q->state == 1)
                {
                    maxNum = Llinfo[q->num].count > Llinfo[maxNum].count ? q->num : maxNum;
                }
                q = q->next;
            }
        }
        p = p->next;
    }
    return maxNum;
}

/***********************
 * param: void
 * return: int(v的编号)
 * res: 返回v的编号，没有就返回0
***********************/
int GetV3(LinkClause C)
{
    LinkClause p = C->next;
    while (p)
    {
        if (p->state == 1)
        {
            LinkLiteral q = p->L->next;
            while (q)
            {
                if (q->state == 1)
                {
                    return q->num;
                }
                q = q->next;
            }
        }
        p = p->next;
    }
    return 0;
}

/***********************
 * param: void
 * return: void
 * res: 打印各文字的值
***********************/
void myPrint(void)
{
    for (int i = 1; i <= n; i++)
    {
        if (Llinfo[i].value == 1)
        {
            printf("%5d", i);
        }
        else
        {
            printf("%5d", -i);
        }
        if (i % 9 == 0 && i != n)
        {
            printf("\n");
        }
    }
    printf("\n");
}

/***********************
 * param: LinkClause(子句头指针)
 * return: Status(表明满足与否)
 * res: 传入子句头指针，返回该cnf文件的满足性
***********************/
Status DPLL(LinkClause C, int idea)
{
    // test
    // printf("cnt = %d\n", _cnt++);
    // 栈的准备
    ClauseStack Cs1, Cs2;
    LiteralStack Ls1, Ls2;
    InitClauseStack(Cs1);
    InitClauseStack(Cs2);
    InitLiteralStack(Ls1);
    InitLiteralStack(Ls2);
    int num, res;
    while ((num = FindSingleClause(C)) != 0)
    {
        DelClauseAndLiteral(C, Cs1, Ls1, num);
    }
    res = isEmptyClause(C);
    if (res == 0)
    {
        // myPrint();
        return TRUE;
    }
    else if (res == 1)
    {
        RecoveryClauseAndLiteral(C, Cs1, Ls1);
        return FALSE;
    }
    // 垃圾策略选择v
    // 忽略了负文字，要提升效率，应该还要确认删除数的符号
    // int v = GetV2(C);
    int v;
    if (idea == 1)
    {
        v = GetV();
    }
    else if (idea == 2)
    {
        v = GetV2(C);
    }
    else
    {
        v = GetV3(C);
    }
    int ans;
    if (v == 0)
    {
        printf("ERROR!!!");
        exit(0);
    }
    // test
    // printf("v: %d\n", v);
    DelClauseAndLiteral(C, Cs2, Ls2, v);
    ans = DPLL(C, idea);
    if (ans == TRUE)
        return TRUE;
    RecoveryClauseAndLiteral(C, Cs2, Ls2);
    DelClauseAndLiteral(C, Cs2, Ls2, -v);
    ans = DPLL(C, idea);
    if (ans == FALSE)
    {
        RecoveryClauseAndLiteral(C, Cs2, Ls2);
        RecoveryClauseAndLiteral(C, Cs1, Ls1);
    }
    return ans;
}

void saveRes(char filename[30], int time)
{
    char str[60] = "s 1\nv";
    int i;
    FILE *fp = fopen(filename, "w");
    fputs(str, fp);
    for (i = 1; i <= n; i++)
    {
        if (Llinfo[i].value == 1)
        {
            fprintf(fp, " %d", i);
        }
        else
        {
            fprintf(fp, " %d", -i);
        }
    }
    fprintf(fp, "\nt %d", time);
    fclose(fp);
}